f:().
(n:. 0  f(n))
 (k:, g:({0..(k+1)}).
 (n:{0..(k+1)}, i:{0..n}. (g(i)) < (g(n)))  0  i < k. f(g(i))  0  i < g(k). f(i)) 

latex

Definitions	a  b, suptype(S; T), S  T, T, P  Q, P  Q, True, x. t(x), P & Q, i  j < k, {i..j}, , False, A, A  B, i  j , , t  T, x(s), P  Q, x:A. B(x), {T}
Lemmas	summand-qle-sum, qle weakening eq qorder, qadd functionality wrt qle, qle functionality wrt implies, sum split q, qadd wf, sum unroll hi q, sum unroll base q, true wf, squash wf, qsum-non-neg, qsum wf, le wf, int seg wf, ge wf, nat properties, rationals wf, int inc rationals, qle wf, nat wf